DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2019.45

Cyclic Proofs and Jumping Automata

Authors: Denis Kuperberg, Laureline Pinault, and Damien Pous

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)

Abstract

We consider a fragment of a cyclic sequent proof system for Kleene algebra, and we see it as a computational device for recognising languages of words. The starting proof system is linear and we show that it captures precisely the regular languages. When adding the standard contraction rule, the expressivity raises significantly; we characterise the corresponding class of languages using a new notion of multi-head finite automata, where heads can jump.

Cite as

Denis Kuperberg, Laureline Pinault, and Damien Pous. Cyclic Proofs and Jumping Automata. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 45:1-45:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kuperberg_et_al:LIPIcs.FSTTCS.2019.45,
  author =	{Kuperberg, Denis and Pinault, Laureline and Pous, Damien},
  title =	{{Cyclic Proofs and Jumping Automata}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{45:1--45:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.45},
  URN =		{urn:nbn:de:0030-drops-116071},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.45},
  annote =	{Keywords: Cyclic proofs, regular languages, multi-head automata, transducers}
}

Search Results

Documents authored by Pinault, Laureline

Cyclic Proofs and Jumping Automata

Abstract

Cite as

Thanks for your feedback!

Could not send message